T:Type, l1,l2,l3:(T List). iseg(T; l1; l2)  iseg(T; l2; l3)  iseg(T; l1; l3) 

latex

Definitions	prop{i:l}, t  T, x:A. B(x), iseg(T; l1; l2), P  Q, x:A. B(x)
Lemmas	append wf, member wf, nat wf, non neg length, length wf1, append assoc